--- Checks for 'TreeMap'
module tests.qc.Map where

import Test.QuickCheck
import Test.QuickCheckArbitrary ()  -- avoid doc error
import Data.TreeMap as TM
import Data.List (elemBy)


aTree = arbitrary :: Gen (TreeMap Int String)
aList = arbitrary :: Gen [(Int, String)]

--- The empty tree is 'TreeMap.Nil'
p_emptyIsNil = once (nil empty) 
    where 
        nil TreeMap.Nil = true
        nil _        = false

--- check if the invariants are maintained
invariants TreeMap.Nil = true
invariants TreeMap.Leaf{} = true
invariants t = not (null t.left && null t.right)
                && invariants t.left
                && invariants t.right

--- the invariants are maintained in arbitrary trees
p_invariants = forAll aTree (\t -> invariants t)

--- An AVL tree is balanced so that the height of the left and right subtree differ by at most 1
p_balance = forAll aTree (\t -> abs t.balance < 2)

--- The height of a tree is 1 more than the maximum of the heights of its subtrees
p_height = forAll aTree (\t ->
    null t && t.height == 0
        || t.{key?} && not t.{left?} && t.height == 1 
        || t.height == 1 + max t.left.height t.right.height)

--- After insertion, a lookup with the same key yields the inserted value        
p_insert = forAll aTree (\t -> 
            forAll Int.arbitrary (\k ->
                forAll String.arbitrary (\v ->
                    let nt = insert k v t in
                        invariants t 
                            && invariants nt 
                            && lookup k nt  == Just v)))

--- After deletion of a key, lookup results in Nothing
p_delete = forAll aTree (\t ->
            not (null t) ==> forAll (elements (keys t)) (\k ->
                let dt = delete k t in
                    invariants t
                        && invariants dt
                        && lookup k dt  == Nothing))

--- After deletion of all keys, a tree is empty
p_deleteAll = forAll aTree (\t ->
    null (fold TreeMap.delete t (keys t)))
    
{-- 
    A tree constructed from a list has only key value pairs that are elements of that list,
    and it has a an entry for every key of the list.
    -}
p_list = forAll aList (\xs ->
    let ys = each (TM.fromList xs)
        eby = elemBy (using fst) 
    in all (`elem` xs) ys && all (`eby` ys) xs) 

--- TreeMap.insertList (TreeMap.insertList Nil xs) ys == TreeMap.insertList Nil (xs ++ ys)
p_insertList = forAll aList (\ys ->
                forAll aList (\xs ->
        let ta = TreeMap.insertList (TreeMap.insertList empty xs) ys 
            tb = TreeMap.insertList empty (xs ++ ys)
        in each ta == each tb))

